\section{Function Contracts}
\label{sect:functions}

Next we turn to the specification of functions. We'll take the example
from the previous section, and pull the computation of the minimum of
two numbers out into a separate function:

\vccInput[linerange={begin-}]{c/3.1.min2.c}

(The listing above presents both the source code and the output
of VCC, typeset in a different fonts, and 
the actual file name of the example is replaced with \vcc{/*`testcase`*/}.)
VCC failed to prove our assertion, even though it's easy to see that
it always holds. This is because verification in VCC is \Def{modular}: 
VCC doesn't look inside the body of a function (such as the definition of \vcc{min()}) 
when understanding the effect of a call to the function (such as 
the call from \vcc{main()});
all it knows about the effect of calling \vcc{min()} is that the call 
satisfies the specification of \vcc{min()}. 
Since the correctness of \vcc{main()} clearly depends on what \vcc{min()}
does, we need to specify \vcc{min()} in order to verify \vcc{main()}.

The specification of a function is sometimes called its \Def{contract},
because it gives obligations on both the function and its callers. It
is provided by four types of annotations:
\begin{itemize}
\item A requirement on the caller (sometimes called a
  \Def{precondition} of the function) takes the form \vcc{_(requires E)}, 
  where \vcc{E} is an expression. It says that callers of the
  function promise that \vcc{E} will hold on function entry. 

\item A requirement on the function (sometimes called a
  \Def{postcondition} of the function) takes the form \vcc{_(ensures E)}, 
  where \vcc{E} is an expression. It says that the function
  promises that \vcc{E} holds just before control exits the
  function. 

\item The third type of contract annotation, a \Def{writes clause}, is described
  in the next section. In this example, the lack of writes clauses says that \vcc{min()}
  has no side effects that are visible to its caller.

\item The last type of contract annotation, a \Def{termination clause},
  is described in section \secref{termination}. For now, we won't bother 
  proving that our functions terminate.
\end{itemize}

For example, we can provide a suitable specification for \vcc{min()} as
follows:
\vccInput[linerange={min-endmin,out-}]{c/3.2.min3.c}
\noindent
(Note that the specification of the function comes after the header and
before the function body; you can also put specifications on function
declarations (\eg in header files).)
The precondition \vcc{_(requires \true)} of \vcc{min()} doesn't
really say anything (since \vcc{\true} holds in every state), but is included
to emphasize that the function can be called from any state and
with arbitrary parameter values.
The postcondition states that the value returned from \vcc{min()} 
is no bigger than either of the inputs.
Note that \vcc{\true} and \vcc{\result} are spelled with a backslash
to avoid name clashes with C identifiers.%
\footnote{
  All VCC keywords start with a backslash; 
  this contrasts with annotation tags (like \vcc{requires}),
  which are only used at the beginning of annotation
  and therefore cannot be confused with C identifiers
  (and thus you are still free to have, \eg
  a function called \lstinline{requires} or \lstinline{assert}).}

VCC uses function specifications as follows. When verifying the body of a
function, VCC implicitly assumes each precondition of the function on
function entry, and implicitly asserts each postcondition of the
function (with \vcc{\result} bound to the return value and each
parameter bound to its value on function entry) just before the
function returns. For every call to the function, VCC replaces the
call with an assertion of the preconditions of the function, sets the
return value to an arbitrary value, and finally assumes each
postcondition of the function. 
For example, VCC translates the program above roughly as follows:
\vccInput[linerange={begin-end}]{c/3.3.min_assert.c}

Note that the assumptions above are ``harmless'', that is in a fully
verified program they will be never violated, as each follows
from the  assertion that proceeds it in an execution%
\footnote{
A more detailed explanation of why this translation is sound is given in section \secref{soundness}.
}% 
For example, the  assumption generated by a precondition could fail only if the 
assertion generated from that same precondition  before it fails.

\begin{note}
\notehd{Why modular verification?}
Modular verification brings several benefits. 
First, it allows verification to more easily scale to
large programs. Second, by providing a precise interface between
caller and callee, it allows you to modify the implementation of
a function like \vcc{min()} without having to worry about breaking the
verifications of functions that call it (as long as you don't change
the specification of \vcc{min()}). This is especially important
because these callers normally aren't in scope, and the person
maintaining \vcc{min()} might not even know about them (e.g., if
\vcc{min()} is in a library). Third, you can verify a function like
\vcc{main()} even if the implementation of \vcc{min()} is unavailable
(\eg if it hasn't been written yet). 
\end{note}

\subsection*{Exercises}
\begin{enumerate}
\item
What is the effect of giving a function the specification
\vcc{_(requires \false)}? How does it effect verification of
the function itself? What about its callers? Can you think of a good 
reason to use such a specification?

\item
Can you see anything wrong with the above specification of \vcc{min()}?
Can you give a simpler implementation than the one presented? Is this 
specification strong enough to be useful? If not, how might it be
strengthened to make it more useful?

\item
Specify a function that returns the (\vcc{int}) square root of its (\vcc{int})
argument. (You can try writing an implementation for the function, but
won't be able to verify it until you've learned about loop
invariants.)

\item
Can you think of useful functions in a real program that might
legitimately guarantee only the trivial postcondition \vcc{_(ensures \true)}?
\end{enumerate}

\subsection*{Solutions}
\begin{enumerate}

\item
Any function with a spec that includes \vcc{_(requires \false)} should
verify. However, a call to such a function will only verify if the
call itself is dead code (and VCC can prove it is dead code). Putting
\vcc{_(requires  \false)} on a function is one way to document that nothing has
been proven about it, and that it should not be called.

\item
The spec guarantees that \vcc{min} returns a result that is small
enough, but nothing prevents it from always returning
\vcc{INT_MIN}. This might be strong enough for some applications, but
for most, you probably want the additional postcondition
\vcc{_(ensures \result == a || \result == b)}.

\item
\begin{VCC}
int sqrt(int x)
_(requires x >= 0)
_(ensures \result * \result <= x && (result + 1) * (\result + 1) > x)
;
\end{VCC}

\item
Many important system functions have no nontrivial guaranteed
postcondition, save those that come from the omission of writes clauses.
For example, a system call that tries to collect garbage might
very well have an empty specification. 
\end{enumerate}

\subsection{Reading and Writing Memory}
\label{sect:writes}

When programming in C, it is important to distinguish two kinds of
memory access. \Def{Sequential} access, which is the default, is appropriate when
interference from other threads (or the outside world) is not an
issue, \eg when accessing unshared memory. Sequential accesses can be
safely optimized by the compiler by breaking it up into multiple
operations, caching reads, reordering operations, and so on. 
\Def{Atomic} access is required when the access might race with other
threads, \ie write to memory that is concurrently read or written,
or a read to memory that is concurrently written. Atomic access is typically
indicated in C by accessing memory through a volatile type (or through atomic 
compiler intrinsics). We consider only sequential 
access for now; we consider atomic access in section \secref{concurrency}.

To access a memory object pointed to by a pointer \vcc{p}, \vcc{p}
must point to a valid chunk of memory%
\footnote{VCC actually enforces a stronger condition, that the memory
  is ``typed'' according to \vcc{p}.
}%
. (For example, on typical hardware, its virtual address must be suitably aligned,
must be mapped to existing physical memory, and so on.) 
In addition, to safely access memory sequentially, the memory must not be concurrently
written by other threads (including hardware and devices). Most of the
time\footnote{
  It is also possible to read memory sequentially if it is a
  nonvolatile field of an object that is known to be closed, even if
  it is not owned by the thread; this allows multiple threads to
  sequentially access shared read-only memory. 
}, this is because the memory object is ``part of'' something that
is ``owned'' by the thread (concepts that will be discussed later);
we express this with the predicate 
\vcc{\thread_local(p)}\footnote{Note that thread locality only makes sense in
the context of a particular thread, and so cannot appear, for example,
in type invariants.} VCC asserts this 
before any sequential memory access to (the memory pointed to by) \vcc{p}.

To write sequentially through \vcc{p}, you need to know \vcc{\thread_local(p)},
and that no other thread is trying to read (sequentially or
concurrently) through \vcc{p} at the same time\footnote{
  You also need to know that no object invariants depend on \vcc{*p}; 
  this is why object invariants are in effect only for closed objects, and only
  (parts of) open objects are mutable.
}. We write this as \vcc{\mutable(p)}. Like thread-locality,
mutability makes sense only in the context of a particular thread.
%%Writing via pointers other than \vcc{p} cannot make \vcc{p} non-mutable.

\begin{note}
If VCC doesn't know why an object is thread local, then it has
hard time proving that the object stays thread local after an operation
with side effects (\eg a function call).
Thus, in preconditions you will sometimes want to use
\vcc{\mutable(p)} instead of \vcc{\thread_local(p)}.
The precise definitions of mutability and thread locality
is given in \secref{ownership},
where we also describe another form of guaranteeing thread locality
through so called ownership domains.
\end{note}

The \vcc{NULL} pointer, pointers outside bounds of arrays,
the memory protected by the operating system, or outside
the address space are never thread local (and thus also never mutable
nor writable).

There is one further restriction on sequential writes, motivated by
the desire to limit the possible side effects of a function call to a
specific set of mutable objects. We could do this by adding a
postcondition that all other parts of the state are unmodified, but
VCC provides some sugar to make specification (and reasoning) about
such properties more convenient and efficient. The idea is that when
you call a function, you give it permission to write certain objects,
but not others; \vcc{\writable(p)} expresses the condition that
the function has the right to write to
\vcc{p}. Thus, when writing through \vcc{p}, VCC asserts
\vcc{\mutable(p) && \writable(p)}.

While mutability is a thread-level concept, writability is a property
of a particular instance of an executing function. (That is, just
because something is writable for you doesn't mean it will be writable
for a function you call.) Therefore, you can't express that a function
needs ``permission'' to write \vcc{p} by 
\vcc{_(requires \writable(p))},
because preconditions are evaluated in the context
of the caller. Instead, you specify that a function needs writability
of \vcc{p} at function entry with the annotation \vcc{_(writes p)},
called a ``writes clause''. When you call a function, VCC assumes that
all of the objects listed in the writes clauses are writable on
function entry.  Moreover, if an object becomes mutable (for a thread)
after entry to a function call, it is considered writable within that
call (as long as it remains mutable).

%Moved this up -E
%Access to thread local memory will never crash the program.
%The memory that is not thread-local is covered in 
%\secref{concurrency}.

Let's have a look at an example:
\vccInput[linerange={begin-}]{c/3.4.rw.c}
\noindent
The function \vcc{write_wrong} fails because \vcc{p} is only
mutable, and not writable.
In \vcc{read_wrong} VCC complains that it does not know
anything about \vcc{p} (maybe it's \vcc{NULL}, who knows),
in particular it doesn't know it's thread-local.
\vcc{read2} is fine because \vcc{\mutable} is stronger
than \vcc{\thread_local}.
Finally, in \vcc{test_them} the first three assertions succeed
because if something is not listed in the writes clause
of the called function it cannot change.
The last assertion fails, because \vcc{write()} listed \vcc{&a}
in its writes clause.

%\noindent Without the \vcc{\thread_local()} annotation you would
%get the following:
%\vccInput[linerange={begin-}]{c/01_read_wrong.c}

% the concept of validity (typed pointers) is gone from VCC3 --MM
%For each memory access within a program, VCC checks that the access is accessing a 
%\Def{valid} memory object. Validity implies that the object address
%points to memory that is actually in the address space of the program
%(i.e., it has been allocated, either on the stack or on the heap, and
%has not been freed). (Validity in VCC additionally requires that the
%access is appropriately typed; this aspect is 
%described in more detail in \secref{type-safety}). 

Intuitively, the clause \vcc{_(writes p, q)} says that, 
of the memory objects that are thread-local to the caller before the call,
the function is going to modify only the object pointed to by \vcc{p}
and the object pointed to by \vcc{q}.
%\todo{I think we should get rid of this footnote. For writes claiuses, the ownership domains
%are logically irrelevant; what matters is when the object became mutable.
%\footnote{
%And their ``ownership domains'',
%but until \secref{ownership} we consider these to be empty.
%}
In other words, it is roughly equivalent to a postcondition that ensures
that all other objects thread-local to the caller prior
to the call remain unchanged.
A function can have multiple writes clauses, and implicitly
combines them into a single set. If a function spec contains no writes clauses, 
it is equivalent to specifying a writes clause with empty set of
pointers.

% Do we have essentially the same paragraph later? -E
%More precisely, an object is \vcc{\writable} if it is \vcc{\mutable} and 
%it is either listed in a writes clause of the function,
%or it became \vcc{\mutable} sometime after the function was entered; the 
%latter condition guarantees that either \vcc{p} was listed in the
%writes clause or was not thread-local in the caller when the call to
%the function was made. 
%In particular, formal function parameters and local variables are
%writable as long as they are in scope and have not been explicitly
%wrapped (\secref{invariants}) or reinterpreted to a
%different type (\secref{reint}).  VCC asserts
%\vcc{\writable(p)} on each attempt to write to \vcc{*p}, as well as on
%each call to a function that lists \vcc{p} in a writes clause.

Here is a simple example of a function that visibly reads and writes
memory; it simply copies data from one location to another.
\vccInput[linerange={begin-}]{c/3.5.copy1.c}
In the postcondition the expression \vcc{\old(E)} returns the value
the expression \vcc{E} had on function entry.
Thus, our postcondition states that the new value of \vcc{*to}
equals the value \vcc{*from} had on call entry. 
VCC translates the function call \vcc{copy(&x,&y)} approximately as
follows:
\begin{VCC}
_(assert \thread_local(&x))
_(assert \mutable(&y))
// record the value of x
int _old_x = x;
// havoc the written variables
havoc(y);
// assume the postcondition
_(assume y == _old_x)
\end{VCC}

%% Shouldn't \array_range be allowed for arrays of non-primitives also?
% Similar to \vcc{\thread_local_array},
%\vcc{\mutable_array(ar,sz)} is defined as
%\vcc{\forall unsigned i; i < sz ==> \mutable(&ar[i])}.
%
%The expression \vcc{\thread_local_array(ar, sz)} is
%syntactic sugar for \vcc{\forall unsigned i; i < sz ==> \thread_local(&ar[i])}.
%
%Programs that manipulate arrays often write to multiple array
%locations. Writes clauses actually allow sets of pointers, rather than
%individual pointers. We'll introduce sets in full generality later, but
%note one special case: the expression \vcc{\array_range(ar, len)}
%denotes the set of pointers \vcc@{&ar[0], &ar[1], ..., &ar[len-1]}@. 
%Thus, a writes clause of the form
%\vcc{_(writes \array_range(ar,len))}
%allows writing to all elements of the array.

\subsubsection{Local Variables}
Unlike most block-structured languages, C allows you to take the
addresses of local variables (with the \vcc{&} operator). If you take
the address of a local, nothing prevents you from storing that address
in a data structure, and trying to dereference the address after the
lifetime of the variable has ended. (The result is not pretty.) Even
if you are careful about its lifetime, once you take the address of a
variable, you have to worry that writing through some seemingly
unrelated pointer might change the value of the variable, which is a
pain.

Because of this, VCC distinguishes between local variables whose
addresses are never taken and those whose addresses are taken; the
former are called \Def{purely local} variables. A purely local
variable is much, much easier to reason about; you know that its value
can be changed only by a an update through its name 
(In particular, it cannot be modified by function calls, by
assignments to other variables, or assignments through pointers.)
Purely local variables are always considered thread-local (so there is
no thread-locality check when reading them) and writable (so you never
have to mention them in writes clauses of loops or blocks). Also, if
you have a loop that doesn't modify a purely local variable in scope,
VCC will automatically infer that the value of that variable is not
changed in the loop. So you should definitely keep variables purely
local whenever possible.

A local variable that is not purely local is treated as if it was
allocated on the heap when its lifetime starts (but without the
possibility of allocation failure), and is freed when the lifetime
ends. 

The treatment of pure locality sometimes results in the strange
phenomenon that changing some code near the end of a function body can
cause verification of someting earlier in the function body to
fail. This is because if you take the address of a local near the
bottom, it is treated as impure for the whole function body. The
simplest workaround in such cases is just to introduce a new local for
the bottom part of the function\footnote{This won't effect the final
binary produced by a decent optimizing compiler.}.

\subsection{Arrays}
\label{sect:arrays}

Array accesses are a kind of pointer accesses.
Thus, before allowing you to read an element of an array VCC checks if it's thread-local.
Usually you want to specify that all elements of an array are thread-local,
which is done using the expression \vcc{\thread_local_array(ar, sz)}.
It is essentially a syntactic sugar for
\vcc{\forall unsigned i; i < sz ==> \thread_local(&ar[i])}.
The annotation \vcc{\mutable_array()} is analogous.
To specify that an array is writable use:
\begin{VCC}
_(writes \array_range(ar, sz))
\end{VCC}
which is roughly a syntactic sugar for:
\begin{VCC}
_(writes &ar[0], &ar[1], ..., &ar[sz-1])
\end{VCC}

For example, the function below is recursive implementation of the 
C standard library \vcc{memcpy()} function:
\vccInput[linerange={begin-end}]{c/3.6.copy_array.c}
It requires that array \vcc{src} is thread-local,
\vcc{dst} is writable, and they do not overlap.
It ensures that, at all indices, \vcc{dst} has the
value \vcc{src}. The next section presents a more conventional implementation using a loop.

\subsection{Termination}
\label{sect:termination}
A function terminates if it is guaranteed to return to its
caller. You can specify termination for simple functions (like the
ones we've seen so far) by simply adding to the specification
\vcc{_(decreases 0)}; this will do the job as long as your functions
are not recursive. For functions that are recursive (or which look
potentially recursive to VCC, because of potential callbacks from
functions whose bodies are hidden from VCC), the termination clause of
a function gives a measure that decreases for each call that might start
a chain of calls back the function. For example, to verify the
termination of \vcc{my_memcpy} above, you need only add to its
specification the additional annotation \vcc{_(decreases len)}. This
annotation defines a ``measure'' on calls to \vcc{my_memcpy} (namely,
the value passed as the last parameter). VCC checks termination 
by checking that (1) all loops in the body terminate
(\secref{loopTermination}), and
(2) for every function call within the body of
\vcc{my_memcpy} that is potentially the first of a chain of calls
leading to a call back to \vcc{my_memcpy}, the called function has a
\vcc{_(decreases)} specification and the measure of the call to that
function is strictly less than the measure of the calling function
instance.  

It is usually a good idea to prove termination for sequential code
when you can\footnote{ You should also consider doing it for your
  concurrent code, but here VCC is much more limited in its
  capabilities. The reason for this is that proving termination for a
  racy function (e.g., one that has to compete for locks) typically
  depends on fairness assumptions (e.g., that a function trying to
  grab a spinlock will eventually get lucky and get it, if the
  spinlock is infinitely often free) and/or global termination
  measures (e.g., to make sure that other threads will release
  spinlocks once they acquire them). VCC does not currently support
  either of these.}.
More details on termination measures can be found in the VCC manual.

\subsection{Pure functions}
\label{sect:pureFunctions}
A \Def{pure function} is one that has no side effects on the program
state. In VCC, pure functions are not allowed to allocate memory, and can
write only to local variables. Only pure functions can be called within VCC
annotations; such functions are required to terminate\footnote{
  This is to guarantee that there is indeed a mathematical function
  satisfying the specification of the function.
}.

The function \vcc{min()} above
example of a function that can be declared to be pure; this is done by
adding the modifier \vcc{_(pure)} to the beginning of the function specification,
\eg
\begin{VCC}
_(pure) min(int x, int y) ...
\end{VCC}

Being pure is a stronger condition that simply having an empty writes
clause. This is because a writes clause has only to mention those side
effects that might cause the caller to lose information (\ie
knowledge) about the state, and as we have seen, VCC takes advantage
of the kind of information callers maintain to limit the kinds of side
effects that have to be reported.

A pure function that you don't want to be executed can be defined
using the \vcc{_(def)} tag, which is essentially a pure ghost function
(one that can be used only in specifications) that is inlined, and
uses the following streamlined syntax:
\vccInput[linerange={beginsp-endsp}]{c/3.7.issorted.c}
\noindent
A partial spec for a sorting routine could look like the following:%
\footnote{We will take care about input being permutation of the output in \secref{ghosts}.}
\vccInput[linerange={beginso-endso}]{c/3.7.issorted.c}


\subsection{Contracts on Blocks} 

Sometimes, a large function will contain an inner block that
implements some simple functionality, but you don't want to refactor
it into a separate function (\eg because you don't want to bother with
having to pass in a bunch of parameters, or because you want to verify
code without rewriting it). VCC lets you conduct your verification as
if you had done so, by putting a function-like specification on the
block. This is done by simply writing function specifications
preceding the block, \eg
\begin{VCC}
...
x = 5;
_(requires x == 5)
_(writes &x)
_(ensures x == 6)
{
  x++;
}
...
\end{VCC}
VCC translates this by (internally) refactoring the block into a
function, the parameters of which are the variables from the
surrounding scope that are mentioned within the block (or the block
specifications), so blocks with contracts cannot have statements that
transfer control outside of the block. The advantages of this
translation is that within the block, VCC can ignore what it knows
about the preceding context, and following the block, VCC can
``forget'' what it knew inside the block (other than what escapes
through the \vcc{ensures} clauses); in each case, this results in less
distracting irrelevant detail for the theorem prover.


Sometimes, you don't care about information flowing into the block,
but only care about the information flowing out of the block. In this
case, you can use the precondition \vcc{_(requires \full_context())},
which tells VCC to verify the block using all of the information about
what came before, but using the postconditions and writes clauses to
hide information about what went on inside the block to the code that
follows the block.

%% \vccInput[linerange={swap-partition}]{c/04_partition.c}
%% \vccInput[linerange={foo-}]{c/01_swap1.c}

%% Because global variables (like \vcc{z}) might be visible to callers
%% of \vcc{copy()}, \vcc{copy()} needs to report that they might change.
%% Note that the writes clause lists pointers to memory locations, not lvalues
%% (\ie \vcc{_(writes &x, &y, &z)} and not \vcc{_(writes x, y, z)}).
%% Note also that because \vcc{&z} aliases neither \vcc{&x} nor \vcc{&y}, VCC can
%% deduce that \vcc{swap(&x, &y)} does not change \vcc{z}.

%% Had we left out the writes clause from the specification of
%% \vcc{swap()}, VCC would report several errors:
%% \vccInput[linerange={out-}]{c/01_swap2.c}
%% \noindent 

%% Whenever a memory object is read, VCC asserts that it is
%% thread-local; whenever a memory object is written or is
%% mentioned in the writes clause of a function call, VCC asserts that it
%% is writable. Try removing each of the function annotations in
%% this example (one at a time) to see what error messages you get.

%% For example, the assert/assume translation of \vcc{swap()} is%
%% \footnote{
%%   VCC does not generate the read and writes checks for the local variable
%%   \vcc{tmp}. Because \vcc{tmp} is a local that never has its address
%%   taken, it can be thought of as remaining in a register, where it is
%%   guaranteed to remain writable.
%% }:

%% \vccInput[linerange={swap-}]{c/01_swap3.c}

%% \noindent
%% As we can see, one effect of \vcc{writes p, q} is the implicit
%% precondition \vcc{requires \writable(p) && \writable(q)}. Such precondition
%% needs to be checked in \vcc{foo()}, at the place where it calls \vcc{swap()}.
%% In other words, the called function can write at most what the caller can write.
%% In particular if we forget to list \vcc{&x} in the writes
%% clause of \vcc{foo()} we would get an error when it tries to call a
%% function that possibly writes \vcc{&x}:

%% \vccInput[linerange={out-}]{c/01_swap4.c}


%% You might wonder why cannot we just have 
%% \vcc{requires \writable(p)} and instead have the specialized writes clause.
%% The reason is that the writes clause also specifies that nothing
%% outside of the writes clause will be changed.
%% This is why we can prove that \vcc{y} is still \vcc{42} after the call
%% to \vcc{boundedIncr(&x)}. 


%A predicate \vcc{\mutable(p)} states that the object pointed to by \vcc{p}
%is allocated, ``belongs'' to the current thread, and is in a ``phase of life''
%that allows for modification.
%We will get into details all of these later.
%For now we just need to know that in order to be able to write to \vcc{*p}
%one needs to know that \vcc{p} was listed in the writes clause \emph{and} \vcc{\mutable(p)}.
%For example, if we remove the \vcc{_(writes ...)} clause from the
%\vcc{boundedIncr()} we get the following output:

